functor Coqize (S : COQIZE_STRUCTS) : COQIZE =
struct
  open S

  structure A = Assem
  val localDebug = ref false
  fun dbpr s = if !localDebug
               then print (s^"\n")
               else ()
  fun rpDot str = 
      let fun filt (#".") = #"_"
	    | filt c = c
      in String.map filt str
      end
 
  fun r2str A.Eax = "eax"
    | r2str A.Ebp = "ebp"
    | r2str A.Ebx = "ebx"
    | r2str A.Ecx = "ecx"
    | r2str A.Edi = "edi"
    | r2str A.Edx = "edx"
    | r2str A.Esi = "esi"
    | r2str A.Esp = "esp"

  fun i2str imm = if imm >= 0
		  then Int.toString(imm)
		  else "(-"^(Int.toString(0 - imm))^")"

  fun instr2str inst = 
      let fun mtch (A.Addr(r1, r2)) = "addr "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Addz(imm, r2)) = "addz "^(i2str imm)^" "^(r2str r2)
	    | mtch (A.Addm(imm, r1, r2)) = "addm "^(i2str imm)^" "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Subr(r1, r2)) = "subr "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Subz(imm, r2)) = "subz "^(i2str imm)^" "^(r2str r2)
	    | mtch (A.Subm(imm, r1, r2)) = "subm "^(i2str imm)^" "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Mulr(r1, r2)) = "mulr "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Mulz(imm, r2)) = "mulz "^(i2str imm)^" "^(r2str r2)
	    | mtch (A.Mulm(imm, r1, r2)) = "mulm "^(i2str imm)^" "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Div(dummy)) = "do NOT support Arithmetic Operation DIV !"

	    | mtch (A.Movld(imm, r1, r2)) = "movld "^(i2str imm)^" "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Movr(r1, r2)) = "movr "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Movst(r1, imm, r2)) = "movst "^(r2str r1)^" "^(i2str imm)^" "^(r2str r2)
	    | mtch (A.Movz(imm, r1, tp)) = "movz "^(i2str imm)^" "^(r2str r1)

	    | mtch (A.Xchg(r1, r2)) = "xchg "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Leab(imm, r1, r2)) = "leab "^(i2str imm)^" "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Leal(lb, r1)) = "leal "^lb^" "^(r2str r1)

	    | mtch (A.Cmpr(r1, r2)) = "cmpr "^(r2str r1)^" "^(r2str r2)
	    | mtch (A.Cmpz(imm, r1)) = "cmpz "^(i2str imm)^" "^(r2str r1)
	    | mtch (A.Push(r1)) = "push "^(r2str r1)
	    | mtch (A.Pop(r1)) = "pop "^(r2str r1)
	    | mtch (A.Leave) = "leave "
			       
	    | mtch (A.Jg(lb1, lb2)) = 
	      let val lb1' = rpDot lb1
		  val lb2' = rpDot lb2
	      in "jg "^lb1'^" "^lb2'
	      end
	    | mtch (A.Je(lb1, lb2)) = 
	      let val lb1' = rpDot lb1
		  val lb2' = rpDot lb2
	      in "je "^lb1'^" "^lb2'
	      end
	    | mtch (A.Jge(lb1, lb2)) = 
	      let val lb1' = rpDot lb1
		  val lb2' = rpDot lb2
	      in "jge "^lb1'^" "^lb2'
	      end
	    | mtch (A.Jmp(lb)) = 
	      let val lb' = rpDot lb
	      in "jmp "^lb'
	      end

	    | mtch (A.Call(lb1, lb2)) = 
	      let val lb1' = rpDot lb1
		  val lb2' = rpDot lb2
	      in "call "^lb1'^" "^lb2'
	      end
	    | mtch (A.Ret(lb)) = "ret "

	    | mtch (A.Malloc(imm, lb, tp)) = 
	      let val lb' = rpDot lb
	      in "malloc "^(i2str imm)^" "^lb'
	      end
	    | mtch (A.Free(r1)) = "free "^(r2str r1)

	    | mtch _ = "????"
      in mtch inst
      end

  fun ppCodeBlock (name, cb) = 
      let val (cb', tlcode) = (fn [] => raise Fail "codeblock is empty\n"
				| t => (List.tl(List.rev(t)), 
					List.hd(List.rev(t)))) cb

	  val tlcode' = instr2str tlcode

	  fun fdFn (inst, rStr) = 
	      let val inst' = instr2str inst
	      in (fn "????" => rStr
		   | t => "seq (\n\t"^t^") ("^rStr^")") inst'
	      end
	  val name' = rpDot name
	  val core = List.foldl fdFn tlcode' cb'
      in "Definition "^name'^" : iseq := \n\t"^core^".\n\n"
      end

  fun ppFCodeHeap (name, lablist, prefix) = 
      let fun fdFn pref (lb, rStr) = 
	      let val lb' = rpDot lb
	      in "consFCH "^lb'^" "^pref^lb'^" \n\t("^rStr^")"
	      end
	  val name' = rpDot name
	  val core = List.foldl (fdFn prefix) "emptyFCH" lablist
      in "\nDefinition "^name'^" : fcodeheap := \n\t"^core^".\n\n"
      end

  fun ppCodeHeap (name, lablist, subfix) =       
      let fun fdFn subf (lb, rStr) = 
	      let val lb' = rpDot lb
	      in "consCH "^lb'^" "^lb'^subf^" \n\t("^rStr^")"
	      end
	  val name' = rpDot name
	  val core = List.foldl (fdFn subfix) "emptyCH" lablist
      in "\nDefinition "^name'^" : codeheap := \n\t"^core^".\n\n"
      end

  fun pr_int i = if(i<0)
	         then ("(-"^Int.toString(Int.abs(i))^")")
	         else Int.toString(i)

  fun pr_etype (A.Int) = "Z"
    | pr_etype (A.Str(s)) = s
    | pr_etype _ = raise Fail "bug in pr_etype\n"

  fun pr_st st = 
      let fun pr (A.Rf(i)) = ("rf"^Int.toString(i), i, 0)
	    | pr (A.Hp(i)) = ("hp"^Int.toString(i), i, 1)
	    | pr (A.Upd(st', e0, e1)) = 
	      let val (sst', isS0, rORh) = pr_st st'
		  val isFlagR = (fn A.Zf => true
				  | A.Sf => true
				  | _ => false) e0

		  val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in if isFlagR
		 then ("writeFR ("^sst'^") ("^str_e0^") ("^str_e1^")", isS0, 0)
		 else ((fn 0 => ("writeR ("^sst'^") ("^str_e0^") ("^str_e1^")", isS0, rORh)
			 | 1 => ("writeM ("^sst'^") ("^str_e0^") ("^str_e1^")", isS0, rORh)
			 | _ => raise Fail "bug\n") (rORh))
	      end
      in  pr st
      end

  and pr_state sta = 
      let val rf = A.getRf sta
	  val hp = A.getHp sta

	  val (rf', i0, d0) = pr_st rf
	  val (hp', i1, d1) = pr_st hp
	  val _ = if i0 <> i1
		  then raise Fail "bug\n"
		  else ()
      in "("^hp'^", "^rf'^")"
      end

  and pr_exp' ep = 
      let fun pr (A.IntNum(i)) = 
	      if(i<0)
	      then ("(-"^Int.toString(Int.abs(i))^")")
	      else Int.toString(i)
	    | pr (A.Mem(ad)) = 
	      if(ad<0)
	      then ("(-"^Int.toString(Int.abs(ad))^")")
	      else Int.toString(ad)
	    | pr (A.Id(str)) = str
	    | pr (A.Plus(e0,e1)) = 
	      let val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in "("^str_e0^"+"^str_e1^")"
	      end 
	    | pr (A.Minus(e0,e1)) = 
	      let val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in "("^str_e0^"-"^str_e1^")"
	      end 
	    | pr (A.Times(e0,e1)) = 
	      let val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in "("^str_e0^"*"^str_e1^")"
	      end 
	    | pr (A.Reg(rg)) = r2str rg
	    | pr (A.Zf) = "zf"
	    | pr (A.Sf) = "sf"

	    | pr (A.State(st)) = pr_state st

            | pr (A.TrForm (s, e)) =
              let val str_e = pr_exp e
              in  s^ "("^str_e^")"
              end
	    | pr _ = raise Fail "bug\n"
      in (fn (A.Sel(st0, e0)) => let val (str_st0, isS0, rORh) = pr_st st0				     
				     val isFlagR = (fn A.Zf => true
						     | A.Sf => true
						     | _ => false) e0
				     val str_e0 = pr_exp e0
				 in if isFlagR
				    then ("(readFR ("^str_st0^") ("^str_e0^"))", 0)
				    else ((fn 0 => ("(readR ("^str_st0^") ("^str_e0^"))", 0)
					    | 1 => ("(readM ("^str_st0^") ("^str_e0^"))", 1)
					    | _ => raise Fail "bug\n") (rORh))
				 end
	   | (A.Some(e1)) => ("Some "^(pr_exp e1), 1)
	   | t => (pr t, 0)) ep
      end

  and pr_exp ep = 
      let val (ep', dummy) = pr_exp' ep
      in ep'
      end


  fun pr_prop pp = 
      let fun pr (A.True) = "True"
	    | pr (A.Imply(p1, p2)) = 
	      let val str_p1 = pr_prop p1
		  val str_p2 = pr_prop p2
	      in "("^str_p1^") -> \n("^str_p2^")"
	      end
	    | pr (A.Not(p1)) = 
	      let val str_p1 = pr_prop p1
	      in "(~"^str_p1^")"
	      end
	    | pr (A.And(p0,p1)) = 
	      let val str_p0 = pr_prop p0
		  val str_p1 = pr_prop p1
	      in "("^str_p0^")/\\("^str_p1^")"
	      end
	    | pr (A.Or(p0,p1)) = 
	      let val str_p0 = pr_prop p0
		  val str_p1 = pr_prop p1
	      in "("^str_p0^")\\/("^str_p1^")"
	      end
	    | pr (A.Gt(e0,e1)) = 
	      let val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in "("^str_e0^")>("^str_e1^")"
	      end
	    | pr (A.Ge(e0,e1)) = 
	      let val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in "("^str_e0^")>=("^str_e1^")"	      
	      end
	    | pr (A.Lt(e0,e1)) = 
	      let val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in  "("^str_e0^")<("^str_e1^")"	      
	      end
	    | pr (A.Le(e0,e1)) = 
	      let val str_e0 = pr_exp e0
		  val str_e1 = pr_exp e1
	      in  "("^str_e0^")<=("^str_e1^")"
	      end
	    | pr (A.Eq(e0,e1)) = 
	      let val (str_e0, d0) = pr_exp' e0
		  val (str_e1, d1) = pr_exp' e1
	      in (fn (0, 0) => "("^str_e0^")=("^str_e1^")"
		   | (0, 1) => raise Fail "maybe bug\n"
		   | (1, 0) => "("^str_e0^")= Some("^str_e1^")"
		   | (1, 1) => "("^str_e0^")=("^str_e1^")"
		   | _ => raise Fail "bug\n") (d0, d1)
	      end
	    | pr (A.Ne(e0,e1)) = 
	      let val (str_e0, d0) = pr_exp' e0
		  val (str_e1, d1) = pr_exp' e1
	      in (fn (0, 0) => "("^str_e0^")<>("^str_e1^")"	      
		   | (0, 1) => raise Fail "maybe bug\n"
		   | (1, 0) => "("^str_e0^")<> Some("^str_e1^")"
		   | (1, 1) => "("^str_e0^")<>("^str_e1^")"
		   | _ => raise Fail "bug\n") (d0, d1)
	      end
            | pr (A.Ex((s, t), p)) =
              let val t' = pr_etype t
                  val p' = pr_prop p
              in  "exists "^s^" : "^t'^",\n("^p'^")"
              end
	    | pr (A.Forall((s, t), p)) = 
	      let val t' = pr_etype t
		  val p' = pr_prop p
	      in "forall "^s^" : "^t'^",\n("^p'^")"
	      end
	    | pr (A.Stack(s1, s2)) = 
	      let val s1' = pr_state s1
		  val s2' = pr_state s2
	      in "Stack ("^s1'^") ("^s2'^")"
	      end
	    | pr (A.GoodFrame(sta, ep)) = 
	      let val sta' = pr_state sta
		  val ep' = pr_exp ep
	      in "Good_Frame ("^sta'^") ("^ep'^")"
	      end
            | pr (A.Tree (st, e, size, offl, offr)) = 
              let val (st', isS0, isM) = pr_st st
                  val str_e = pr_exp e
                  val size' = pr_int size
                  val offl' = pr_int offl
                  val offr' = pr_int offr
              in  "Tree("^st'^") ("^str_e^") ("^size'^") ("^offl'^") ("^offr'^")"
              end
            | pr (A.List (st, e, size, off)) =
              let val (st', isS0, isM) = pr_st st
                  val str_e = pr_exp e
                  val size' = pr_int size
                  val off' = pr_int off
              in  "List("^st'^") ("^str_e^") ("^size'^") ("^off'^")"
              end
            | pr (A.InDomM (s, e)) =
              let val str_s = pr_state s
                  val str_e = pr_exp e
              in  "lookupS ("^str_s^") ("^str_e^")"
              end
            | pr (A.NotInDomM (s, e)) =
              let val str_s = pr_state s
                  val str_e = pr_exp e
              in  "notindomS ("^str_s^") ("^str_e^")"
              end
	    | pr _ = "NOT finish yet\n"

      in pr pp
      end

  fun ppAsst (ctname, p) = 
      let val st0 = A.setSt {hp = A.Hp(0), rf = A.Rf(0)}
	  val st1 = A.setSt {hp = A.Hp(1), rf = A.Rf(1)}
	  val p' = p st0 st1
          val _ = dbpr ("ppAsst enter : "^ ctname)
	  val str_p = pr_prop p'
      in "\nDefinition "^ctname^" : assert := \n"
	 ^"fun s0 s1 : state => let (hp0, rf0) := s0 in (let (hp1, rf1) := s1 in (\n\t"
	 ^str_p^")).\n\n"
      end

  fun ppFCodeHeapType (fctname, lablist, prefix) = 
      let fun fdFn pref (lb, rStr) = 
	      let val lb' = rpDot lb
	      in "consFCT "^lb'^" "^pref^lb'^" \n\t("^rStr^")"
	      end
	  val fctname' = rpDot fctname
	  val core = List.foldl (fdFn prefix) "emptyFCT" lablist
      in "\nDefinition "^fctname'^" : fcodeheapty := \n\t"^core^".\n\n"
      end

  fun ppCodeHeapType (ctname, lablist, postfix) = 
      let fun fdFn subf (lb, rStr) = 
	      let val lb' = rpDot lb
	      in "consCT "^lb'^" "^lb'^subf^" \n\t("^rStr^")"
	      end
	  val ctname' = rpDot ctname
	  val core = List.foldl (fdFn postfix) "emptyCT" lablist
      in "\nDefinition "^ctname'^" : codeheapty := \n\t"^core^".\n\n"
      end

  fun ppSigma (signame, lablist, prefixPre, prefixPost) = 
      let fun fdFn (pref, postf) (lb, rStr) = 
	      let val lb' = rpDot lb
		  val fspec = "(fnspec "^pref^lb'^" "^postf^lb'^")"
	      in "consSG "^lb'^" "^fspec^" \n\t("^rStr^")"
	      end

	  val core = List.foldl (fdFn (prefixPre, prefixPost)) "emptySG" lablist
      in "\nDefinition "^signame^" : sigmma := \n\t"^core^".\n\n"
      end

  fun ppCbLem (fname, lab, cbLemName, ctname, fctPostfix, signame, cbTpPrefix, cbPrefix) =
      let val lab' = rpDot lab
          val fname' = rpDot fname 
          val LemName = cbLemName lab'
          val fct = fname'^fctPostfix
          val cbTp = cbTpPrefix ^ lab'
          val cb = cbPrefix ^ lab'
      in  "\nLemma "^LemName^" : \n"^
          "  lookupCT "^ctname^" "^fname'^" "^fct^" ->\n"^
          "    Infer "^ctname^" "^fname'^" "^signame^" "^cbTp^" "^cb^".\n"
      end

  fun ppLab (lab, id) =
      let val lab' = rpDot lab
          val id' = Int.toString id
      in  "Notation "^ lab' ^"\t:= "^ id' ^" (only parsing).\n"
      end

  fun ppArgList arglist = 
      let val argsstr = String.concat (List.map ppArg arglist)
      in  "["^argsstr^"]"
      end
  and ppArg arg =
      (case arg
        of A.O s => s^" "
         | A.L al => (ppArgList al)^" "
         | A.P [] => raise Fail "no such use"
         | A.P [a] => raise Fail "no such use"
         | A.P [a1, a2] => (ppArg a1)^" | "^(ppArg a2)
         | A.P (a :: al) => (ppArg a) ^ " | "^ (ppArg (A.P al)))

  fun ppTactic tac = 
      let fun pr tt =
              (case tt
                of A.Tproof => "Proof"
                 | A.Tqed => "Qed"
                 | A.Tapply (rule, []) => "apply "^rule
                 | A.Tapply (rule, arglist) =>
                   let val str_p = 
                           String.concat 
		               (List.map (fn (pname, pt) => 
				             ("("^pname^":="^pt^") ")) arglist)
                   in "apply "^rule^" with "^str_p
                   end
                 | A.Tintros [] => "intros"
                 | A.Tintros arglist =>
                   let val str_p = 
                           String.concat
                               (List.map (fn(s) =>" "^s) arglist)
                   in "intros"^str_p
                   end
                 | A.Tinversion_clear (s, []) => "inversion_clear"^s
                 | A.Tinversion_clear (s, arglist) =>
                   let val argstr = ppArgList arglist
                   in  "inversion_clear "^ s ^ " as "^ argstr
                   end
                 | A.Tauto => "auto"
                 | A.Tunfold s => "unfold "^s
                 | A.Tseq tlist => 
                   let val _= dbpr " enter seq"
                       fun p [] = raise Fail "no such case"
                         | p [a] = raise Fail "no such case"
                         | p [a1, a2] = (pr a1) ^ "; "^ (pr a2)
                         | p (a :: al) = (pr a) ^"; "^ (p al)
                   in  p tlist
                   end
                 | A.Tor (t1, t2) =>
                   let val t1str = pr t1
                       val t2str = pr t2
                   in  t1str ^ " || " ^ t2str
                   end
                 | A.Tpara tlist =>
                   let fun p [] = raise Fail "no such case"
                         | p [a] = raise Fail "no such case"
                         | p [a1, a2] = (pr a1) ^ " | "^ (pr a2)
                         | p (a :: al) = (pr a) ^" | "^ (p al)
                   in  "["^(p tlist)^"]"
                   end
                 | A.Tsplit => "split"
                 | A.Texists s => "exists ("^s^")"
                 | A.TexistsS (hp, rf) =>
                   let val (hps, _, _) = pr_st hp
                       val (rfs, _, _) = pr_st rf
                   in  "exists ("^hps^", "^rfs^")"
                   end
                 | A.Trepeat t => 
                   let val _ = dbpr "enter repeat"
                       val _ = case t
                                of A.Trepeat _ => dbpr "sub tactic is repeat"
                                 | A.Tseq _ => dbpr "sub tactic is seq"
                                 | _ => dbpr "sub tactic is others"
                       val tstr = pr t
                       val _ = dbpr "out repeat\n"
                   in  "repeat ("^tstr^")"
                   end 
                 | A.Tconstructor => "constructor"
                 | A.Ttry t =>
                   let val tstr = pr t
                   in  "try ("^ tstr ^ ")"
                   end
                 | A.Tomega => "omega"
                 | A.TtacIn (t, s) =>
                   let val tstr = pr t
                   in  tstr ^" in "^s
                   end
                 | A.Tinduction (s, []) => "induction "^s
                 | A.Tinduction (s, arglist) =>
                   let val argstr = ppArgList arglist
                   in  "induction "^ s ^ " as "^ argstr
                   end
                 | A.Tdestruct (s, []) => "destruct "^s
                 | A.Tdestruct (s, arglist) =>
                   let val argstr = ppArgList arglist
                   in  "destruct "^ s ^ " as "^ argstr
                   end
                 | A.Tsimpl => "simpl"
                 | A.Tassert (s, a)=>
                   let val ass = pr_prop a
                   in  "assert ("^s^" : "^ass^")"
                   end
                 | A.Tclear s => "clear "^s
                 | A.Treflexivity => "reflexivity"
                 | A.Treplace (e1, e2) => 
                   let val e1s = pr_exp e1
                       val e2s = pr_exp e2
                   in  "replace ("^e1s^") with ("^e2s^")"
                   end
                 | A.Trewrite s => "rewrite "^s
                 | A.Tinjection s => "injection "^s
                 | A.Tcut s => "cut ("^s^")")
          val retv = (pr tac)^".\n"
          val _ = dbpr retv
      in  retv
      end

end
